package karpiel.boguchwal.wojciech.przemek

import karpiel.boguchwal.wojciech.przemek.Ast._
import karpiel.boguchwal.wojciech.przemek.Bruinizer._
import org.scalatest.FunSuite

class BruinizerTest extends FunSuite {
  test("testBruinize") {
    assertThrows[Exception](bruinize(Var("dd"))(Context.Empty, RealCache()))
    assert(bruinize(Var("dd"))(Context.Empty.append(BoolType, "dd")(RealCache()), RealCache()) == Bruijn(0, Some("dd")))
    assert(bruinize(PiValue(NamedType("xD", BoolType), Var("xD")))(Context.Empty, RealCache()) ==
      PiValue(BoolType, Bruijn(0, Some("xD"))))

    assert(bruinize(PiValue(NamedType("xD", BoolType), PiValue(NamedType("qwe", UnitType), Var("xD"))))(Context.Empty, RealCache()) ==
      PiValue(BoolType, PiValue(UnitType, Bruijn(1, Some("xD")))))
    assert(bruinize(PiValue(NamedType("xD", BoolType), PiValue(NamedType("xD", UnitType), Var("xD"))))(Context.Empty, RealCache()) ==
      PiValue(BoolType, PiValue(UnitType, Bruijn(0, Some("xD"))))) //shadow variable

    assert(bruinize(PiValue(NamedType("xD", BoolType), IdType(BoolTrue, Refl(Var("xD")))))(Context.Empty, RealCache()) ==
      PiValue(BoolType, IdType(BoolTrue, Refl(Bruijn(0, Some("xD"))))))
  }


  test("z czytajmnie") {
    implicit val cace: Cache = RealCache()
    implicit val ctx: Context = Context.Empty
    assert(Bruinizer.bruinize(PiValue(NamedType("A", Universe(0)), PiValue(NamedType("x", Var("A")), Var("x")))) == PiValue(Universe(0), PiValue(Bruijn(0, Some("A")), Bruijn(0, Some("x")))))
    assert(Bruinizer.bruinize(PiElim(PiValue(NamedType("A", Universe(0)), PiValue(NamedType("x", Var("A")), Var("x"))), UnitType)) == PiElim(PiValue(Universe(0), PiValue(Bruijn(0, Some("A")), Bruijn(0, Some("x")))), UnitType))
    assert(Bruinizer.bruinize(PiElim(PiElim(PiValue(NamedType("A", Universe(0)), PiValue(NamedType("x", Var("A")), Var("x"))), UnitType), UnitValue)) == PiElim(PiElim(PiValue(Universe(0), PiValue(Bruijn(0, Some("A")), Bruijn(0, Some("x")))), UnitType), UnitValue))
  }
}
